%
% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
%
% SPDX-License-Identifier: BSD-2-Clause
%

@string{sv = "Springer"}
@string{acmpress = "ACM"}
@string{proc = "Proceedings of the "}
@string{itp = "International Conference on Interactive Theorem Proving"}
@string{itp12 = proc#"3rd "#itp}
@string{lncs = "Lecture Notes in Computer Science"}

@misc{autocorres,
    author={David Greenaway},
    title={{AutoCorres} tool},
    url= {https://trustworthy.systems/projects/TS/autocorres/},
    year = 2016,
    note = {Accessed May 2016},
    doi = {10.5281/zenodo.11248},
}

@misc{CParser_download,
  author = {Michael Norrish},
  title = {{C-to-Isabelle} Parser, version 1.13.0},
  year = 2013,
  month = may,
  url = {https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md},
  note = {Accessed May 2016}
}

@book{C11,
    title = {{ISO}/{IEC} 9899:2011 Information technology --- Programming languages --- {C}},
    author = {{ISO}},
    publisher = {International Organization for Standardization},
    institution = {ISO/IEC JTC 1/SC 22},
    year = 2011,
    note = {``The C11 Standard''}
}

@article{Simpl-AFP,
    author  = {Norbert Schirmer},
    title   = {A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment},
    journal = {Archive of Formal Proofs},
    month   = feb,
    year    = 2008,
    url     = {https://www.isa-afp.org/entries/Simpl.html},
    note    = {Formal proof development},
    ISSN    = {2150-914X},
}

@article{Separation_Algebra-AFP,
    author  = {Gerwin Klein and Rafal Kolanski and Andrew Boyton},
    title   = {Separation Algebra},
    journal = {Archive of Formal Proofs},
    month   = may,
    year    = 2012,
    url     = {https://www.isa-afp.org/entries/Separation_Algebra.html},
    note    = {Formal proof development},
    ISSN    = {2150-914x},
}

@article{Greenaway_AK_12,
    publisher        = sv,
    isbn             = {978-3-642-32346-1},
    series           = lncs,
    format           = {pdf},
    author           = {David Greenaway and June Andronick and Gerwin Klein},
    year             = 2012,
    month            = aug,
    volume           = 7406,
    editor           = {Lennart Beringer and Amy Felty},
    title            = {Bridging the Gap: Automatic Verified Abstraction of {C}},
    booktitle        = itp12,
    pages            = {99-115},
    address          = {Princeton, New Jersey},
    url              = {https://trustworthy.systems/publications/nicta_full_text/5662.pdf}
}

@article{Greenaway_LAK_14,
    publisher        = acmpress,
    doi              = {10.1145/2594291.2594296},
    author           = {Greenaway, David and Lim, Japheth and Andronick, June and Klein, Gerwin},
    month            = jun,
    nictapubid       = {7629},
    pages            = {429--439},
    year             = {2014},
    title            = {Don't Sweat the Small Stuff: Formal Verification of {C} Code Without the Pain},
    type             = {Conference Paper},
    booktitle        = {Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation},
    address          = {Edinburgh, UK},
    url              = {https://trustworthy.systems/publications/nicta_full_text/7629.pdf}
}
